R:Realizer, i:Id. R-has-loc(R;i)   

latex

Definitions	Realizer, t  T, Id, Knd, type List, x:A. B(x), a = b, IdLnk, Type, x. t(x), a:A fp B(a), Prop, x:AB(x), State(ds), DeclaredType(ds;x), x:AB(x), source(l), , p  q, false, x,y,z. t(x;y;z), x,y,z,w,v. t(x;y;z;w;v), x,y,z,u,v,w. t(x;y;z;u;v;w), x,y,z,w. t(x;y;z;w), es realizer ind, R-has-loc(R;i)
Lemmas	es realizer ind wf, bfalse wf, bor wf, bool wf, lsrc wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, eq id wf, Knd wf, Id wf, es realizer wf